T:Type, ll:(T List List), x:T.
(x  concat(ll))
 (ll1,ll2:T List List
 ((l1,l2:T List
 (((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2))  (T List)
 ((& ll = (ll1 @ [(l1 @ [x] @ l2)] @ ll2)))) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), P & Q, P  Q, , P  Q, t  T, x. t(x), Top, S  T, P  Q, as @ bs, Y, {T}, x(s)
Lemmas	all functionality wrt iff, iff wf, l member wf, concat wf, append wf, iff functionality wrt iff, member-concat, l member decomp, length wf nat, top wf, nat wf, concat append, concat-cons, concat-nil, append nil sq, member wf, and functionality wrt iff, iff transitivity, member append, or functionality wrt iff, cons member